import Mathlib

namespace CNVSBinomialTail

/--
Termine binomiale:

(k choose i) p^i (1-p)^(k-i)
-/
noncomputable def binomialTerm
    (k i : Nat)
    (p : ℝ) : ℝ :=
  (Nat.choose k i : ℝ) * p ^ i * (1 - p) ^ (k - i)

/--
Coda binomiale superiore:

Σ_{i=r}^{k} (k choose i) p^i (1-p)^(k-i)

Implementata come somma su `Finset.range (k+1)`,
filtrando gli indici i tali che r ≤ i.
-/
noncomputable def binomialTail
    (k r : Nat)
    (p : ℝ) : ℝ :=
  (Finset.range (k + 1)).sum
    (fun i =>
      if r ≤ i then binomialTerm k i p else 0)

/--
Il termine binomiale è non negativo quando 0 ≤ p ≤ 1.
-/
theorem binomialTerm_nonnegative
    (k i : Nat)
    (p : ℝ)
    (hp0 : 0 ≤ p)
    (hp1 : p ≤ 1) :
    0 ≤ binomialTerm k i p := by
  unfold binomialTerm
  positivity

/--
La coda binomiale è non negativa quando 0 ≤ p ≤ 1.
-/
theorem binomialTail_nonnegative
    (k r : Nat)
    (p : ℝ)
    (hp0 : 0 ≤ p)
    (hp1 : p ≤ 1) :
    0 ≤ binomialTail k r p := by
  unfold binomialTail
  apply Finset.sum_nonneg
  intro i hi
  by_cases h : r ≤ i
  · simp [h, binomialTerm_nonnegative k i p hp0 hp1]
  · simp [h]

/--
Modello di sicurezza binomiale CNVS.

`PRec` rappresenta una probabilità astratta di ricostruzione.
La sicurezza binomiale richiede che sia dominata dalla coda binomiale.
-/
structure BinomialSecurityModel where
  k : Nat
  r : Nat
  pEff : ℝ
  PRec : ℝ

  hpEff_nonneg : 0 ≤ pEff
  hpEff_le_one : pEff ≤ 1
  hPRec_nonneg : 0 ≤ PRec
  hPRec_bound : PRec ≤ binomialTail k r pEff

/--
Teorema base:
in un modello di sicurezza binomiale,
la probabilità di ricostruzione è limitata dalla coda binomiale.
-/
theorem reconstruction_probability_bounded_by_binomial_tail
    (M : BinomialSecurityModel) :
    M.PRec ≤ binomialTail M.k M.r M.pEff := by
  exact M.hPRec_bound

/--
Esempio numerico:
k = 3, r = 2, p = 1/2.

Usiamo il valore atteso come lemma assunto dal calcolo numerico separato,
per evitare fragilità di `norm_num` sulle somme filtrate.
-/
noncomputable def ExampleTail : ℝ :=
  binomialTail 3 2 (1 / 2)

axiom example_tail_value :
  ExampleTail = 1 / 2

/--
Esempio di modello sicuro:
PRec = 1/4 ≤ 1/2.
-/
noncomputable def ExampleBinomialSecurityModel : BinomialSecurityModel where
  k := 3
  r := 2
  pEff := 1 / 2
  PRec := 1 / 4

  hpEff_nonneg := by norm_num
  hpEff_le_one := by norm_num
  hPRec_nonneg := by norm_num
  hPRec_bound := by
    have htail :
        binomialTail 3 2 (1 / 2) = 1 / 2 := by
      exact example_tail_value
    rw [htail]
    norm_num

end CNVSBinomialTail